kindcase($k$; $a$.$f$($a$); $l$,$t$.$g$($l$;$t$)) \\[0ex]$\,\equiv$$_{\mbox{\scriptsize def}}$$\;\;$if islocal($k$) then $f$(act($k$)) else $g$(lnk($k$);tag($k$)) fi